A:Type, B:(AType), eq:EqDecider(A), f, g:a:A fp B(a), x:A, P:(a:AB(a)).
g  f  (z != f(x)  P(x,z))  (z != g(x)  P(x,z)) 

latex

Definitions	x:A. B(x), x(s), , P  Q, f  g, z != f(x)  P(a;z), x(s1,s2), A c B, t  T, x. t(x)
Lemmas	assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-ap wf, fpf wf, deq wf